/-
Copyright (c) 2025 Rémy Degenne. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Rémy Degenne, Peter Pfaffelhuber
-/
module

public import Mathlib.MeasureTheory.SetSemiring
public import Mathlib.MeasureTheory.Measure.AddContent
public import Mathlib.MeasureTheory.Measure.Trim

/-!
# Carathéodory's extension theorem

Let `C` be a semiring of sets and `m` an additive content on `C`, which is sigma-subadditive.
Then all sets in the sigma-algebra generated by `C` are Carathéodory measurable with respect to
the outer measure induced by `m`. The induced outer measure is equal to `m` on `C`.

## Main declarations

* `MeasureTheory.AddContent.measureCaratheodory`:
  Construct a measure from a sigma-subadditive function on a semiring. This
  measure is defined on the associated Carathéodory sigma-algebra.
* `MeasureTheory.AddContent.measure`: Construct a measure from a sigma-subadditive content
  on a semiring, assuming the semiring generates a given measurable structure. The measure is
  defined on this measurable structure.

## Main results
* `MeasureTheory.AddContent.inducedOuterMeasure_eq`: The outer measure induced by
  a sigma-subadditive content on a semiring is equal to the content on the sets of the semiring.
* `MeasureTheory.AddContent.isCaratheodory_inducedOuterMeasure_of_mem`: all sets of the semiring are
  Carathéodory measurable with respect to the outer measure induced by a sigma-subadditive content.
* `MeasureTheory.AddContent.isCaratheodory_inducedOuterMeasure`: all sets of the sigma-algebra
  generated by the semiring are Carathéodory measurable with respect to the outer measure induced
  by a sigma-subadditive content.
* `MeasureTheory.AddContent.measureCaratheodory_eq`: The measure
  `MeasureTheory.AddContent.measureCaratheodory` generated from an `m : AddContent C`
  on a `IsSetSemiring C` coincides with `m` on `C`.
* `MeasureTheory.AddContent.measure_eq`: The measure defined through a sigma-subadditive
  content on a semiring coincides with the content on the semiring.
-/

@[expose] public section

open Set

open scoped ENNReal

namespace MeasureTheory.AddContent

variable {α : Type*} {C : Set (Set α)} {s : Set α}

/-- For `m : AddContent C` sigma-sub-additive, finite on `C`, the `OuterMeasure` given by `m`
coincides with `m` on `C`. -/
theorem ofFunction_eq (hC : IsSetSemiring C) (m : AddContent C)
    (m_sigma_subadd : m.IsSigmaSubadditive) (m_top : ∀ s ∉ C, m s = ∞) (hs : s ∈ C) :
    OuterMeasure.ofFunction m addContent_empty s = m s := by
  refine le_antisymm (OuterMeasure.ofFunction_le s) ?_
  rw [OuterMeasure.ofFunction_eq_iInf_mem _ _ m_top]
  refine le_iInf fun f ↦ le_iInf fun hf ↦ le_iInf fun hs_subset ↦ ?_
  calc m s = m (s ∩ ⋃ i, f i) := by rw [inter_eq_self_of_subset_left hs_subset]
    _ = m (⋃ i, s ∩ f i) := by rw [inter_iUnion]
    _ ≤ ∑' i, m (s ∩ f i) := by
      refine m_sigma_subadd (fun i ↦ hC.inter_mem _ hs _ (hf i)) ?_
      rwa [← inter_iUnion, inter_eq_self_of_subset_left hs_subset]
    _ ≤ ∑' i, m (f i) := by
      refine ENNReal.summable.tsum_le_tsum (fun i ↦ ?_) ENNReal.summable
      exact addContent_mono hC (hC.inter_mem _ hs _ (hf i)) (hf i) Set.inter_subset_right

/-- For `m : AddContent C` sigma-sub-additive, finite on `C`, the `inducedOuterMeasure` given by `m`
coincides with `m` on `C`. -/
theorem inducedOuterMeasure_eq (hC : IsSetSemiring C) (m : AddContent C)
    (m_sigma_subadd : m.IsSigmaSubadditive) (hs : s ∈ C) :
    inducedOuterMeasure (fun x _ ↦ m x) hC.empty_mem addContent_empty s = m s := by
  suffices inducedOuterMeasure (fun x _ ↦ m x) hC.empty_mem addContent_empty s = m.extend hC s by
    rwa [m.extend_eq hC hs] at this
  refine Eq.trans ?_ ((m.extend hC).ofFunction_eq hC ?_ ?_ hs)
  · congr
  · intro f hf hf_mem
    rw [m.extend_eq hC hf_mem]
    refine (m_sigma_subadd hf hf_mem).trans_eq ?_
    congr with i
    rw [m.extend_eq hC (hf i)]
  · exact fun _ ↦ m.extend_eq_top _

theorem isCaratheodory_ofFunction_of_mem (hC : IsSetSemiring C) (m : AddContent C)
    (m_top : ∀ s ∉ C, m s = ∞) (hs : s ∈ C) :
    (OuterMeasure.ofFunction m addContent_empty).IsCaratheodory s := by
  rw [OuterMeasure.isCaratheodory_iff_le']
  intro t
  conv_rhs => rw [OuterMeasure.ofFunction_eq_iInf_mem _ _ m_top]
  refine le_iInf fun f ↦ le_iInf fun hf ↦ le_iInf fun hf_subset ↦ ?_
  let A : ℕ → Finset (Set α) := fun i ↦ hC.disjointOfDiff (hf i) (hC.inter_mem _ (hf i) _ hs)
  have h_diff_eq_sUnion i : f i \ s = ⋃₀ A i := by simp [A, IsSetSemiring.sUnion_disjointOfDiff]
  classical
  have h_m_eq i : m (f i) = m (f i ∩ s) + ∑ u ∈ A i, m u :=
    eq_add_disjointOfDiff_of_subset hC (hC.inter_mem (f i) (hf i) s hs) (hf i) inter_subset_left
  simp_rw [h_m_eq]
  rw [ENNReal.tsum_add]
  refine add_le_add ?_ ?_
  · refine iInf_le_of_le (fun i ↦ f i ∩ s) <| iInf_le_of_le ?_ le_rfl
    rw [← iUnion_inter]
    exact Set.inter_subset_inter_left _ hf_subset
  · apply le_trans <| (OuterMeasure.ofFunction m addContent_empty).mono
      <| (iUnion_diff s f) ▸ diff_subset_diff_left hf_subset
    simp only [OuterMeasure.measureOf_eq_coe, A]
    apply le_trans <| measure_iUnion_le (μ := OuterMeasure.ofFunction m addContent_empty)
      (fun i ↦ f i \ s)
    apply ENNReal.tsum_le_tsum
    intro i
    simp_rw [sUnion_eq_biUnion] at h_diff_eq_sUnion
    rw [h_diff_eq_sUnion]
    obtain h6 := MeasureTheory.measure_biUnion_finset_le
      (μ := OuterMeasure.ofFunction m addContent_empty) (A i) id
    simp only [id_eq] at h6
    exact le_trans h6 <| Finset.sum_le_sum <| fun b _ ↦ OuterMeasure.ofFunction_le b

/-- Every `s ∈ C` for an `m : AddContent C` with `IsSetSemiring C` is Carathéodory measurable
with respect to the `inducedOuterMeasure` from `m`. -/
theorem isCaratheodory_inducedOuterMeasure_of_mem (hC : IsSetSemiring C) (m : AddContent C)
    {s : Set α} (hs : s ∈ C) :
    (inducedOuterMeasure (fun x _ ↦ m x) hC.empty_mem addContent_empty).IsCaratheodory s :=
  isCaratheodory_ofFunction_of_mem hC (m.extend hC) (fun _ ↦ m.extend_eq_top hC) hs

theorem isCaratheodory_inducedOuterMeasure (hC : IsSetSemiring C) (m : AddContent C)
    (s : Set α) (hs : MeasurableSet[MeasurableSpace.generateFrom C] s) :
    (inducedOuterMeasure (fun x _ ↦ m x) hC.empty_mem addContent_empty).IsCaratheodory s := by
  induction hs with
  | basic u hu => exact isCaratheodory_inducedOuterMeasure_of_mem hC m hu
  | empty => exact OuterMeasure.isCaratheodory_empty _
  | compl t _ h => exact OuterMeasure.isCaratheodory_compl _ h
  | iUnion f _ h => exact OuterMeasure.isCaratheodory_iUnion _ h

/-- Construct a measure from a sigma-subadditive content on a semiring. This
measure is defined on the associated Carathéodory sigma-algebra. -/
noncomputable def measureCaratheodory (m : AddContent C) (hC : IsSetSemiring C)
    (m_sigma_subadd : m.IsSigmaSubadditive) :
    @Measure α (inducedOuterMeasure (fun x _ ↦ m x) hC.empty_mem addContent_empty).caratheodory :=
  letI : MeasurableSpace α :=
    (inducedOuterMeasure (fun x _ ↦ m x) hC.empty_mem addContent_empty).caratheodory
  { inducedOuterMeasure (fun x _ ↦ m x) hC.empty_mem addContent_empty with
    m_iUnion := fun f hf hd ↦ OuterMeasure.iUnion_eq_of_caratheodory _ hf hd
    trim_le := by
      apply le_inducedOuterMeasure.mpr fun s hs ↦ ?_
      have hs_meas : MeasurableSet[(inducedOuterMeasure (fun x _ ↦ m x) hC.empty_mem
          addContent_empty).caratheodory] s := by
        change (inducedOuterMeasure (fun x _ ↦ m x) hC.empty_mem addContent_empty).IsCaratheodory s
        exact isCaratheodory_inducedOuterMeasure_of_mem hC m hs
      rw [OuterMeasure.trim_eq _ hs_meas, m.inducedOuterMeasure_eq hC m_sigma_subadd hs] }

/-- The measure `MeasureTheory.AddContent.measureCaratheodory` generated from an
`m : AddContent C` on a `IsSetSemiring C` coincides with the `MeasureTheory.inducedOuterMeasure`. -/
theorem measureCaratheodory_eq_inducedOuterMeasure (hC : IsSetSemiring C) (m : AddContent C)
    (m_sigma_subadd : m.IsSigmaSubadditive) :
    m.measureCaratheodory hC m_sigma_subadd s
      = inducedOuterMeasure (fun x _ ↦ m x) hC.empty_mem addContent_empty s := rfl

theorem measureCaratheodory_eq (m : AddContent C) (hC : IsSetSemiring C)
    (m_sigma_subadd : m.IsSigmaSubadditive) (hs : s ∈ C) :
    m.measureCaratheodory hC m_sigma_subadd s = m s :=
  m.inducedOuterMeasure_eq hC m_sigma_subadd hs

/-- Construct a measure from a sigma-subadditive content on a semiring, assuming the semiring
generates a given measurable structure. The measure is defined on this measurable structure. -/
noncomputable def measure [mα : MeasurableSpace α] (m : AddContent C) (hC : IsSetSemiring C)
    (hC_gen : mα ≤ MeasurableSpace.generateFrom C) (m_sigma_subadd : m.IsSigmaSubadditive) :
    Measure α :=
  (m.measureCaratheodory hC m_sigma_subadd).trim <|
    fun s a ↦ isCaratheodory_inducedOuterMeasure hC m s (hC_gen s a)

/-- The measure defined through a sigma-subadditive
  content on a semiring coincides with the content on the semiring. -/
theorem measure_eq [mα : MeasurableSpace α] (m : AddContent C) (hC : IsSetSemiring C)
    (hC_gen : mα = MeasurableSpace.generateFrom C) (m_sigma_subadd : m.IsSigmaSubadditive)
    (hs : s ∈ C) :
    m.measure hC hC_gen.le m_sigma_subadd s = m s := by
  rw [measure, trim_measurableSet_eq]
  · exact m.measureCaratheodory_eq hC m_sigma_subadd hs
  · rw [hC_gen]
    apply MeasurableSpace.measurableSet_generateFrom hs

end MeasureTheory.AddContent
